\begin{tabbing}
es{-}update{-}iff(${\it es}$;$i$;$x$;${\it ds}$;$e$.$P$($e$);$s$.$f$($s$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)\+
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]($P$($e$) $\Rightarrow$ ($x$ after $e$) $=$ $f$((state when $e$))) \& ($\neg$$P$($e$) $\Rightarrow$ ($x$ after $e$) $=$ ($x$ when $e$))
\-\-
\end{tabbing}